mcsta/modest mcsta embedded.jani -E MAX_COUNT=8,T=12 --props up_time -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --alg OptimisticValueIteration --epsilon 1e-6 --width 1e-6 --relative-width --p0 --p1
embedded.jani:model: info: embedded is a CTMC model.
embedded.jani: info: Need 16 bytes per state.
embedded.jani: info: Explored 5820 states for MAX_COUNT=8, T=12.0.
Peak memory usage: 55 MB
Analysis results for embedded.jani
Experiment MAX_COUNT=8, T=12.0
+ State space exploration
State size: 16 bytes
States: 5820
Transitions: 5820
Branches: 16788
Rate: 84348 states/s
Time: 0.1 s
+ Property up_time
Value: 477.5524361629013
Bounds: [477.55195881071614, 477.55291351508646]
Time: 34.3 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 0.0 s
Min. prob. 1 states: 5820
Time for min. prob. 1 states: 0.0 s
+ Essential states
Iterations: 1
Essential states: 2666
Transitions: 2666
Branches: 13634
Time: 0.0 s
+ Optimistic value iteration
Total iterations: 237934
Verif. attempts: 13
Verif. iterations: 18943
Final epsilon: 5.492401449591025E-11
Time: 34.3 s
Exported results to file "/out.txt".